Equational Logic ---------------- <!-- SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain. SPDX-License-Identifier: CC0-1.0 --> [(Up)](../../README.md#topics) | _See also: [Logic](../Logic/README.md#logic), [Term Rewriting](../Term%20Rewriting/README.md#term-rewriting), [Universal Algebra](../Universal%20Algebra/README.md#universal-algebra)_ - - - - ### Web resources [Equational Logic \-- from Wolfram MathWorld](https://mathworld.wolfram.com/EquationalLogic.html) ★ [Equational logic - Wikipedia](https://en.wikipedia.org/wiki/Equational_logic) [Algebraic theory - Wikipedia](https://en.wikipedia.org/wiki/Algebraic_theory) [predicate logic - Give an equational proof \$ \\vdash (\\forall x)(A \\rightarrow B) \\equiv ((\\exists x) A) \\rightarrow B\$ - Mathematics Stack Exchange](https://math.stackexchange.com/questions/751922/give-an-equational-proof-vdash-forall-xa-rightarrow-b-equiv-exists) ★ [elementary set theory - Can I deduce one set distributive law from the other? - Mathematics Stack Exchange](https://math.stackexchange.com/questions/4757220/can-i-deduce-one-set-distributive-law-from-the-other) ★ [Robbins algebra - Wikipedia](https://en.wikipedia.org/wiki/Robbins_algebra) ### Formal Verification of Equational Theories [lo.logic - Formal verification of simple equational proofs (as in Universal Algebra\...)? - MathOverflow](https://mathoverflow.net/questions/71265/formal-verification-of-simple-equational-proofs-as-in-universal-algebra) ★ _(in [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving))_ [Robbins Algebras are Boolean](https://www.cs.unm.edu/~mccune/papers/robbins/) ★ [ðŸ’](commentary/cpressey.md#robbins-algebras-are-boolean) ### Papers [Equational Logic and Abstract Algebra](http://sections.maa.org/florida/proceedings/2001/ramsamujh.pdf) ★★★ [ðŸ’](commentary/cpressey.md#equational-logic-and-abstract-algebra) [Equational logic, unification and term rewriting](https://www2.math.uu.se/~palmgren/tillog/equlogic07.pdf) ★★ [Field Guide to Equational Logic](https://www.sciencedirect.com/science/article/pii/074771719290013T) ★★ [ðŸ’](commentary/cpressey.md#field-guide-to-equational-logic) [Equational Logic (Course Notes, USC, Spring 2017)](https://people.math.sc.edu/mcnulty/alglatvar/equationallogic.pdf) ★★ [ðŸ’](commentary/cpressey.md#equational-logic-course-notes-usc-spring-2017) [Euclid's Elements as an Equational Theory](http://boole.stanford.edu/pub/USyd2015.pdf) ★ [Meadows and the Equational Specification of Division](https://arxiv.org/abs/0901.0823v1) ★ [Survey of the Equational Programming Project](https://people.cs.uchicago.edu/~odonnell/OData/Technical_Papers/Survey_ELP/description.html) ★ [ðŸ’](commentary/cpressey.md#survey-of-the-equational-programming-project) [Programming with Equations](https://www.cs.purdue.edu/cgvlab/www/publications/hoffmann1982programming/) ★ [ðŸ’](commentary/cpressey.md#programming-with-equations) [Second-Order Equational Logic](https://www.cl.cam.ac.uk/~mpf23/papers/Types/soeqlog.pdf) _(in [Type Theory](../Type%20Theory/README.md#type-theory))_ Observational Equality, Now! (online @ [strictlypositive.org](http://strictlypositive.org/obseqnow.pdf)) [ðŸ’](commentary/cpressey.md#observational-equality-now) ### Books Equational Logic as a Programming Language (online @ [archive.org](https://archive.org/details/equational-logic-as-a-programming-language)) (borrow @ [archive.org](https://archive.org/details/equationallogica0000odon)) ★ [ðŸ’](commentary/cpressey.md#equational-logic-as-a-programming-language) Canonical Equational Proofs (borrow with print disabilities @ [archive.org](https://archive.org/details/canonicalequatio0000bach)) [ðŸ’](commentary/cpressey.md#canonical-equational-proofs) _(in [Logic](../Logic/README.md#logic))_ Handbook of logic in artificial intelligence and logic programming, Vol 1 (borrow with print disabilities @ [archive.org](https://archive.org/details/handbookoflogici0001unse)) ★ [ðŸ’](commentary/cpressey.md#handbook-of-logic-in-artificial-intelligence-and-logic-programming-vol-1)